Termination Proof Script

Consider the TRS R consisting of the rewrite rules


1:		app(p,app(s,x))	→ x
2:		app(fact,0)	→ app(s,0)
3:		app(fact,app(s,x))	→ app(app(*,app(s,x)),app(fact,app(p,app(s,x))))
4:		app(app(*,0),y)	→ 0
5:		app(app(*,app(s,x)),y)	→ app(app(+,app(app(*,x),y)),y)
6:		app(app(+,x),0)	→ x
7:		app(app(+,x),app(s,y))	→ app(s,app(app(+,x),y))

There are 11 dependency pairs:


8:		APP(fact,0)	→ APP(s,0)
9:		APP(fact,app(s,x))	→ APP(app(*,app(s,x)),app(fact,app(p,app(s,x))))
10:		APP(fact,app(s,x))	→ APP(*,app(s,x))
11:		APP(fact,app(s,x))	→ APP(fact,app(p,app(s,x)))
12:		APP(fact,app(s,x))	→ APP(p,app(s,x))
13:		APP(app(*,app(s,x)),y)	→ APP(app(+,app(app(*,x),y)),y)
14:		APP(app(*,app(s,x)),y)	→ APP(+,app(app(*,x),y))
15:		APP(app(*,app(s,x)),y)	→ APP(app(*,x),y)
16:		APP(app(*,app(s,x)),y)	→ APP(*,x)
17:		APP(app(+,x),app(s,y))	→ APP(s,app(app(+,x),y))
18:		APP(app(+,x),app(s,y))	→ APP(app(+,x),y)

The approximated dependency graph contains 2 SCCs: {18} and {9,11,13,15}.

Consider the SCC {18}. The constraints could not be solved.

Consider the SCC {9,11,13,15}. The constraints could not be solved.

Tyrolean Termination Tool (0.08 seconds) --- May 3, 2006